T:Type, L:(T List), P:({x:T| (x  L)} prop{i:l}). l-all(L; x.P(x))  l_all(L; T; x.P(x)) 

latex

Definitions	t  T, x:A. B(x), x. t(x), P  Q, P  Q, Y, True, P  Q, reduce(f; k; as), x(s), l-all(L; x.P(x)), P  Q, prop{i:l}, l_all(L; T; x.P(x)), A c B, x:A. B(x), (x  l),
Lemmas	l all wf, true wf, l all nil, l all cons, l member wf, l-all wf, iff functionality wrt iff, list-subtype, select wf, length wf1